import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertFalse;
import static org.junit.Assert.assertSame;

import java.io.File;
import java.io.IOException;

import model.BasicParameter;
import model.cnf.CNF;
import model.cnf.FileCNF;
import model.preprocessor.IllegalPreProcessorParameterException;
import model.preprocessor.PreProcessorParameter;
import model.preprocessor.PreProcessorResult;
import model.preprocessor.PreProcessorResultStatus;

import org.junit.Before;
import org.junit.Test;

import controller.preprocessor.Hypre;


public class TestHypre {

	private File precDirectory;
	private Hypre sat ;
	
	@Before
	public void setUp(){
		try {
			precDirectory = new File("preproc");
			
			sat = new Hypre(precDirectory);
		} catch (IOException e) {
			e.printStackTrace();
			return;
		}
	}
	
	@Test
	public void testHypre(){
		assertFalse("hypre don't use timeout", sat.hasTimeout());
	}
		
	@Test
	public void testGetCommandLine(){
		String cnfFile = "./tstcnf/unsat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getHypreParameter();
		param.setTimeOut(4000);
		param.setOut(out);
		
		String[] tab = sat.getCommandLine(cnfFile);
		assertEquals("wrong parameter : wrong path", tab[0], sat.getPath());
		assertEquals("wrong parameter : wrong output parameter", tab[1], "-o");
		assertEquals("wrong parameter : wrong dest", tab[2], out);
		assertEquals("wrong parameter : wrong source", tab[3], cnfFile);
		
	}
	
	@Test
	public void testDetectUnsat(){
		String cnfFile = "./tstcnf/unsat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param =  sat.getHypreParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
	
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			e.printStackTrace();
			return;
		}
		assertEquals("doesn't detect cnf is unsat", PreProcessorResultStatus.UNSATISFIABLE, res.getStatus());
		
		assertFalse("doen't delete the preprocessor.dat file",new File("preprocessor.dat").isFile());
	}
	
	@Test
	public void testSatInstance(){
		String cnfFile = "./tstcnf/sat.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param = sat.getHypreParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			e.printStackTrace();
			return;
		}
		assertSame("problem with sat instance", PreProcessorResultStatus.SATISFIABLE, res.getStatus());
		assertFalse("doen't delete the preprocessor.dat file",new File("preprocessor.dat").isFile());
	}
	

	@Test
	public void testTimeOut(){
		String cnfFile = "./tstcnf/galerehypre.cnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param =  sat.getHypreParameter();
		param.setTimeOut(BasicParameter.MIN_DELAY);
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			//e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (Exception e) {
			//e.printStackTrace();
			return;
		}
		assertSame("problem with the use of timeout", PreProcessorResultStatus.TIMEOUT_REACHED, res.getStatus());
		assertFalse("doen't delete the preprocessor.dat file",new File("preprocessor.dat").isFile());
	}
	
	@Test
	public void testCNFDoesntExist(){
		String cnfFile = "./tstcnf";
		String out = "./cnf/newcnf.cnf";
		PreProcessorParameter param =  sat.getHypreParameter();
		param.setOut(out);
		CNF cnf;
		try {
			cnf = new FileCNF(cnfFile);
		} catch (Exception e) {
			//e.printStackTrace();
			return;
		}
		
		PreProcessorResult res;
		try {
			res = sat.evaluate(cnf);
		} catch (IllegalPreProcessorParameterException e) {
			e.printStackTrace();
			return;
		}
		
		//attention si machine trop rapide peut poser pb
		assertSame("problem with the use of timeout", PreProcessorResultStatus.PROBLEM, res.getStatus());
		assertFalse("doen't delete the preprocessor.dat file",new File("preprocessor.dat").isFile());
	}
	
	
	
}
